[Merged by Bors] - feat: values of `preAleph.symm` by vihdzp · Pull Request #39713 · leanprover-community/mathlib4

vihdzp · 2026-05-22T15:50:19Z

For a cardinal c, preAleph.symm c returns the ordinal index of c, within the well-order of cardinals.

github-actions · 2026-05-22T15:51:51Z

PR summary da04ff8299

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsInaccessible.preAleph_symm_eq_ord
+ preAleph_natCast
+ preAleph_ofNat
+ preAleph_symm_aleph
+ preAleph_symm_aleph0
+ preAleph_symm_natCast
+ preAleph_symm_ofNat
+ preAleph_symm_univ

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

…nprover-community#39609) The aim of this PR is to make tweaks to imports to make the *rebuild* time shorter by making more use of the module system. This is measured in the "lakeprof" report in the radar: https://speed.lean-lang.org/mathlib4-out/396c763262259f066f3837c32643dd752994ca6d/ The first block shows the longest pole when building mathlib, and the second shows it when a rebuild occurs; and as a result of this PR, the relative difference is increased by quite a bit. Note that the "lakeprof/longest rebuild path//wall-clock" is somewhat noisy, but the relative difference should be measured with somewhat less noise. This was done manually, by taking the second-slowest file in the rebuild path, and tweaking imports around it.

…eanprover-community#37627) We mark `Ideal.primeHeight` as `private`, making `Ideal.height` the only public definition for heights of (prime) ideals. This makes the API more consistent and stops contributors from adding more declarations involving `Ideal.primeHeight`, which should instead be formulated in terms of `Ideal.height`. To relate `Ideal.height` to the order theoretic `Order.height` in the lattice of prime ideals `PrimeSpectrum` we add a lemma `PrimeSpectrum.height_eq_orderHeight`.

…leton_of_discreteTopology` (leanprover-community#39511) This proof can be rewritten into a single use of `grind` that is almost identical and maybe more clear with the purpose of the rewrites.

…nprover-community#39581)

…mmunity#38723) Add `RingEquiv.euclideanDomain` similar to other `RingEquiv` transport lemmas. Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)> Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

…eanprover-community#39715) This PR prepares for leanprover-community#39039 by adding the required syntax. Once this PR is in, we'll do a global find and replace for changing `convert` to `convert!` (without changing the behaviour), and finally we will enable the new behaviour for `convert`. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

…ommunity#39281) Construct the ring structure on algebra homs `C → A` where `C` is a bialgebra and `A` an algebra, and also the ring structure on bialgebra homs `C → A` where `C` and `A` are bialgebras. From Toric Co-authored-by: Michał Mrugała <kiolterino@gmail.com>

…mber ⊤` and other small lemmas (leanprover-community#38424) - Golf `isEmpty_of_colorable_zero` and rename to `Colorable.isEmpty` - `colorable_one_iff`: `G.Colorable 1 ↔ G = ⊥` - Combine `chromaticNumber_eq_zero_of_isEmpty`/`isEmpty_of_chromaticNumber_eq_zero` into `chromaticNumber_eq_zero_iff : G.chromaticNumber = 0 ↔ IsEmpty V` and deprecate the `→` side - `chromaticNumber_top_eq_enat_card`: `chromaticNumber ⊤ = ENat.card V` - Tag `chromaticNumber_top_eq_top_of_infinite`/`chromaticNumber_eq_zero_of_isEmpty` as `simp` - Golf `chromaticNumber_eq_one_iff`

…ty lemmas (leanprover-community#39008) This adds some more API for multiplicities of prime ideals in factorizations (and some more basic API lemmas, too), in preparation for a proof of the Northcott property for heights on number fields. We also extend the API for `HasFinite{Mul|}Support` a bit.

…enContFract (leanprover-community#37997) Let $g$ be a `GenContFract K`. In this PR I generalize the determinant formula for continued fractions from the simple continued fraction case $$A_n B_{n+1} - B_n A_{n+1} = (-1)^n$$ to the generalized continued fraction product formula $$A_n B_{n+1} - B_n A_{n+1} = (-a_0) (-a_1) \dots (-a_n)$$ - The `SimpContFract` version is still available unchanged, so this should avoid breaking existing users of the old API. - The use of `0` as the default partial numerator in `(g.partNums.get? i).getD 0` allows product formulation that remains valid when the fraction is terminated. Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

…-community#39721) This PR makes any use of `convert` pop up a "Try this:" message replacing it with `convert!`. This prepares for leanprover-community#39039 which will make `convert` change behaviour and `convert!` retain the old behaviour. Note that `convert` and `convert!` still do the same thing and result in the same goals after this PR is applied, except `convert!` does not pop up a "Try this:" afterwards. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

…the presentation of the union (over the disjoint union of generators) (leanprover-community#38866) Co-authored-by: j-mayoral <marvinsettembrini@gmail.com>

We also deprecate a bunch of theorems that now follow from the typeclass.

…prover-community#39462)

…unity#39463) In this file, we introduce a typeclass `SSet.Nonsingular` for a simplicial set `X : SSet`: it says that for any non-degenerate simplex `x : X _⦋n⦌`, the corresponding morphism `Δ[n] ⟶ X` is a monomorphism.

@su00000

…cal property (leanprover-community#39109) We show that if there exists a set `{ r }` of `R` such that `Mᵣ` is a finitely presented `Rᵣ`-module for each `r`, then `M` is a finitely presented `R`-module. From the [Local Properties of Modules](https://github.com/mbkybky/module_localProperties) project. - [x] depends on: leanprover-community#39112 Co-authored-by: Sihan Su @su00000 <ssh@stu.pku.edu.cn> Co-authored-by: Yi Song @syur2 <sif4delta0@mail.ustc.edu.cn>

…allyReduced` (leanprover-community#39138) Refactor `Algebra.IsGeometricallyReduced` to adapt to a general algebra over commutative ring. In the up-coming leanprover-community#39141, we prove that this definition makes the base change to any field reduced.

…community#39422) Also adds the missing n-ary product lemmas to match the existing sum lemmas. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>

…ra (leanprover-community#39483) Adds the cocommutative coalgebra and bialgebra structure on `SymmetricAlgebra R M` following`MonoidAlgebra` precedent.

…eanprover-community#39601) Also adds `r ∈ spectrum R B ↔ ¬IsUnit (B.charpoly.eval r)` which is the ring version of `r ∈ spectrum K A ↔ A.charpoly.IsRoot r`.

…nprover-community#39604)

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

…ndom variables (leanprover-community#38754) If `X` and `Y` are independent then `∫ ω, X ω * Y ω ∂μ = ∫ ω, X ω ∂μ * ∫ ω, Y ω ∂μ`. We generalize this to the case of a general continuous bilinear map, and specialize it for scalar multiplication and multiplication.

…rover-community#39594) We add `BinaryFan.IsLimit.lift` as the analogue to `Fan.IsLimit.lift` and `BinaryFan.isLimitMapConeEquiv` as the analogue to `Fan.isLimitMapConeEquiv`. We also add the dual versions.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

…9854) These exist more generally in the setting of `SuccAddOrder`.

…er-community#39893) - refactors `Convex/Birkhoff` by removing the `Linarith` import and shortening the support-shrinking argument in `doublyStochastic_sum_perm_aux` Extracted from leanprover-community#37968 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

…ver-community#39859) We want to write `x + 1` instead of `succ x`. These were three easy pickings.

There was an extraneous apostrophe.

YaelDillies

Aren't you missing "inaccessible" in your PR description?

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

vihdzp · 2026-05-28T17:42:20Z

No, the PR description doesn't require an inaccessible cardinal. e.g. preAleph.symm ℵ₁ = ω + 1 since ℵ₁ is the (ω + 1)-th cardinal.

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2026-05-28T20:54:21Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

b-mehta

Thanks!

bors d+

mathlib-bors · 2026-05-29T01:21:42Z

✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

…ealeph

vihdzp · 2026-05-29T07:05:47Z

bors r+

For a cardinal `c`, `preAleph.symm c` returns the ordinal index of `c`, within the well-order of cardinals. Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> Co-authored-by: Aaron Liu <aaronliu2008@outlook.com> Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Co-authored-by: Thomas Browning <13339017+tb65536@users.noreply.github.com> Co-authored-by: Yi.Yuan <kysyy1@126.com> Co-authored-by: mathlib-splicebot[bot] <261196803+mathlib-splicebot[bot]@users.noreply.github.com> Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> Co-authored-by: Wenrong Zou <141128015+WenrongZou@users.noreply.github.com> Co-authored-by: Manuel Candales <42380156+manuelcandales@users.noreply.github.com> Co-authored-by: Sebastien Gouezel <10818434+sgouezel@users.noreply.github.com> Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Co-authored-by: Lua Viana Reis <me@lua.blog.br> Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com> Co-authored-by: mathlib-update-dependencies[bot] <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <10105016+grunweg@users.noreply.github.com> Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com> Co-authored-by: Garmelon <11077553+Garmelon@users.noreply.github.com> Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> Co-authored-by: Jon Eugster <9141564+joneugster@users.noreply.github.com> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Bhavik Mehta <29959226+b-mehta@users.noreply.github.com> Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Co-authored-by: Xavier Généreux <20421163+xgenereux@users.noreply.github.com> Co-authored-by: Weiyi Wang <wwylele@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

mathlib-bors · 2026-05-29T07:38:39Z

Pull request successfully merged into master.

Build succeeded:

plp127 · 2026-05-29T10:21:33Z

why are there 2292 changed files

For a cardinal `c`, `preAleph.symm c` returns the ordinal index of `c`, within the well-order of cardinals. Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> Co-authored-by: Aaron Liu <aaronliu2008@outlook.com> Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Co-authored-by: Thomas Browning <13339017+tb65536@users.noreply.github.com> Co-authored-by: Yi.Yuan <kysyy1@126.com> Co-authored-by: mathlib-splicebot[bot] <261196803+mathlib-splicebot[bot]@users.noreply.github.com> Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> Co-authored-by: Wenrong Zou <141128015+WenrongZou@users.noreply.github.com> Co-authored-by: Manuel Candales <42380156+manuelcandales@users.noreply.github.com> Co-authored-by: Sebastien Gouezel <10818434+sgouezel@users.noreply.github.com> Co-authored-by: Justus Springer <50165510+justus-springer@users.noreply.github.com> Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com> Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com> Co-authored-by: Lua Viana Reis <me@lua.blog.br> Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com> Co-authored-by: mathlib-update-dependencies[bot] <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com> Co-authored-by: Michael Rothgang <10105016+grunweg@users.noreply.github.com> Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com> Co-authored-by: Garmelon <11077553+Garmelon@users.noreply.github.com> Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com> Co-authored-by: Jon Eugster <9141564+joneugster@users.noreply.github.com> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Bhavik Mehta <29959226+b-mehta@users.noreply.github.com> Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> Co-authored-by: Xavier Généreux <20421163+xgenereux@users.noreply.github.com> Co-authored-by: Weiyi Wang <wwylele@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

vihdzp added 2 commits May 22, 2026 09:46

prove thms

f9e689b

golf

49d3ce8

github-actions Bot added the t-set-theory Set theory label May 22, 2026

b-mehta and others added 26 commits May 22, 2026 16:23

chore(Topology): remove repeated grind from `DenselyOrdered.subsing…

de290dd

…leton_of_discreteTopology` (leanprover-community#39511) This proof can be rewritten into a single use of `grind` that is almost identical and maybe more clear with the purpose of the rewrites.

feat(LinearAlgebra/Matrix/SpecialLinearGroup): Add action on R^n (lea…

c94e7c7

…nprover-community#39581)

feat(PresentedGroup): free-product of presentations is isomorphic to …

889ec7b

…the presentation of the union (over the disjoint union of generators) (leanprover-community#38866) Co-authored-by: j-mayoral <marvinsettembrini@gmail.com>

chore: IsBotZeroClass (Fin n) (leanprover-community#39058)

3459947

We also deprecate a bunch of theorems that now follow from the typeclass.

feat(AlgebraicTopology/SimplicialSet): more API for PairingCore (lean…

ec2d568

…prover-community#39462)

feat: IsBotOneClass (Associates M) (leanprover-community#39059)

ad74f63

feat: add congruence lemmas for (d)finsupp big operators (leanprover-…

504fc86

…community#39422) Also adds the missing n-ary product lemmas to match the existing sum lemmas. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@u-paris.fr>

feat(RingTheory): cocommutative bialgebra structure on SymmetricAlgeb…

e449c72

…ra (leanprover-community#39483) Adds the cocommutative coalgebra and bialgebra structure on `SymmetricAlgebra R M` following`MonoidAlgebra` precedent.

feat(LinearAlgebra/Matrix/Charpoly/Eigs): generalize to CommRings (l…

9eb40b4

…eanprover-community#39601) Also adds `r ∈ spectrum R B ↔ ¬IsUnit (B.charpoly.eval r)` which is the ring version of `r ∈ spectrum K A ↔ A.charpoly.IsRoot r`.

chore(GroupTheory/QuotientGroup/Basic): remove transitive import (lea…

95a4c73

…nprover-community#39604)

feat(AlgebraicGeometry/Birational/RationalMap): add `RationalMap.repr…

7f2af3f

…esentative` (leanprover-community#39656) Split off from leanprover-community#39317

chore(CategoryTheory/Limits): some API for binary (co)products (leanp…

5e77d5c

…rover-community#39594) We add `BinaryFan.IsLimit.lift` as the analogue to `Fan.IsLimit.lift` and `BinaryFan.isLimitMapConeEquiv` as the analogue to `Fan.isLimitMapConeEquiv`. We also add the dual versions.

chore: cleanup Integral file (leanprover-community#39652)

04f69b5

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

vihdzp and others added 4 commits May 27, 2026 17:34

chore: deprecate duplicate theorems on ENat (leanprover-community#3…

4b5956c

…9854) These exist more generally in the setting of `SuccAddOrder`.

chore: deprecate three lemmas about Order.succ on ordinals (leanpro…

3c3bbad

…ver-community#39859) We want to write `x + 1` instead of `succ x`. These were three easy pickings.

doc(SetTheory/Cardinal/Aleph): fix typo (leanprover-community#39860)

d6340e9

There was an extraneous apostrophe.

vihdzp requested a review from YaelDillies May 27, 2026 21:33

YaelDillies reviewed May 28, 2026

View reviewed changes

Comment thread Mathlib/SetTheory/Cardinal/Regular.lean Outdated

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label May 28, 2026

YaelDillies self-assigned this May 28, 2026

Update Mathlib/SetTheory/Cardinal/Regular.lean

d0a8597

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

vihdzp removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 28, 2026

YaelDillies approved these changes May 28, 2026

View reviewed changes

YaelDillies removed their assignment May 28, 2026

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 28, 2026

b-mehta reviewed May 29, 2026

View reviewed changes

Comment thread Mathlib/SetTheory/Cardinal/Aleph.lean

mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 29, 2026

vihdzp added 2 commits May 29, 2026 01:03

Merge branch 'prealeph' of https://github.com/vihdzp/mathlib4 into pr…

7ac1ea6

…ealeph

ofNat

da04ff8

mathlib-bors Bot changed the title ~~feat: values of preAleph.symm~~ [Merged by Bors] - feat: values of preAleph.symm May 29, 2026

mathlib-bors Bot closed this May 29, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - feat: values of `preAleph.symm`#39713

[Merged by Bors] - feat: values of `preAleph.symm`#39713
vihdzp wants to merge 145 commits into
leanprover-community:masterfrom
vihdzp:prealeph

vihdzp commented May 22, 2026

Uh oh!

github-actions Bot commented May 22, 2026 •

edited

Loading

Declarations diff

Uh oh!

YaelDillies left a comment

Uh oh!

Uh oh!

vihdzp commented May 28, 2026

Uh oh!

YaelDillies left a comment

Uh oh!

github-actions Bot commented May 28, 2026

Uh oh!

b-mehta left a comment

Uh oh!

Uh oh!

mathlib-bors Bot commented May 29, 2026

Uh oh!

vihdzp commented May 29, 2026

Uh oh!

mathlib-bors Bot commented May 29, 2026

Uh oh!

plp127 commented May 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

Uh oh!

Conversation

vihdzp commented May 22, 2026

Uh oh!

github-actions Bot commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary da04ff8299

Import changes for modified files

Declarations diff

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

vihdzp commented May 28, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented May 28, 2026

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors Bot commented May 29, 2026

Uh oh!

vihdzp commented May 29, 2026

Uh oh!

mathlib-bors Bot commented May 29, 2026

Uh oh!

plp127 commented May 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

20 participants

github-actions Bot commented May 22, 2026 •

edited

Loading